package br.cin.ufpe.rabbit;

import gov.nasa.jpf.Config;

import gov.nasa.jpf.JPF;
import gov.nasa.jpf.jvm.MethodInfo;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.tool.RunJPF;
import gov.nasa.jpf.util.Pair;

import java.io.BufferedReader;
import java.io.IOException;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.lang.reflect.Modifier;
import java.util.List;
import java.util.concurrent.Callable;
import java.util.concurrent.CompletionService;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorCompletionService;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;

import br.cin.ufpe.rabbit.RabbitConfig.ExecutionMode;


final class JPFExecution implements Callable<String> {
	Main.Search mode;
	Config config;

	public JPFExecution(Config config, Main.Search mode) {
		this.mode = mode;
		this.config = config;
	}

	public String call() {
		Process theProcess = null;
		// BufferedReader inStream = null;
		// call the Hello class
		try {
			theProcess = Runtime.getRuntime().exec(
					"java gov.nasa.jpf.tool.RunJPF");
		} catch (IOException e) {
			System.err.println("Error on exec() method");
			e.printStackTrace();
		}

		// theProcess.

		return "Run";
	}
}

// this class shouldn be used.
public class Main {

	static final String JPF_CLASSNAME = "gov.nasa.jpf.JPF";
	static final String DFS_CLASSNAME = "gov.nasa.jpf.search.DFSearch";
	static final String BFS_CLASSNAME = "gov.nasa.jpf.search.heuristic.BFSHeuristic";
	static final String DFS_HEU_CLASSNAME = "gov.nasa.jpf.search.heuristic.DFSHeuristic";

	public static void main(String args[]) throws InterruptedException,
			ExecutionException {

		// final Config config = new Config(args);
		final Config config2 = new Config(args);

		// ExecutorService threadPool = Executors.newFixedThreadPool(2);
		// CompletionService<String> pool = new
		// ExecutorCompletionService<String>(threadPool);

		Thread t1 = new Thread(new Runnable() {
			public void run() {
				Process theProcess = null;
				BufferedReader inStream = null;

				try {
					theProcess = Runtime.getRuntime().exec("java JPFProcess");
				} catch (IOException e) {
					System.err.println("Error on exec() method");
					e.printStackTrace();
				}
				try {
					inStream = new BufferedReader(new java.io.InputStreamReader(
							theProcess.getInputStream()));
					System.out.println(inStream.readLine());
				} catch (IOException e) {
					System.err.println("Error on inStream.readLine()");
					e.printStackTrace();
				}
			}
		});

		Thread t2 = new Thread(new Runnable() {
			public void run() {

			}
		});
		t1.start();
		System.out.println("rodou t1");
		// t1.join();
		t2.start();

		// pool.submit(new JPFExecution(config,Search.DFS));
		// pool.submit(new JPFExecution(config2,Search.BFS));

		// try{
		// String result = pool.take().get();
		// result += pool.take().get();
		// }catch (Throwable e) {
		// System.out.println(e.getCause().getMessage());
		// e.getCause().printStackTrace();
		// }

		// threadPool.shutdown();

		// br.cin.ufpe.rabbit.RabbitConfig.executionMode =
		// ExecutionMode.valueOf(config.getString("EXECUTION.MODE",br.cin.ufpe.rabbit.RabbitConfig.executionMode.toString()));

		// switch (br.cin.ufpe.rabbit.RabbitConfig.executionMode) {
		// //case
		// break;
		// case DOUBLE:
		// // first JPF Execution, just to run YoshiListener
		// runListener(config, args);
		// // JPF Execution with Yoshi Search
		// String[] argv = getHeuristicArgs(config);
		// dump();
		//
		//
		// RunJPF.main(argv);
		// break;
		// case SINGLE:
		// RunJPF.main(args);
		// break;
		// default:
		// throw new UnsupportedOperationException();
		//
		// }
	}

	static enum Search {
		DFS, DFS_HEU, BFS
	}

	static void runJPF(Config config, Search search) {
		String[] argv;
		switch (search) {
		case DFS:
			argv = configJPFArgs(config, DFS_CLASSNAME);
			RunJPF.main(argv);
			break;

		case BFS:
			argv = configJPFArgs(config, BFS_CLASSNAME);
			RunJPF.main(argv);
			break;
		default:
			break;
		}

	}

	static String[] configJPFArgs(Config config, String search) {
		String[] ret = new String[6];
		ret[0] = "+target=" + config.getTarget();

		String target_args = "";
		for (String string : config.getTargetArgs()) {
			if (string != null)
				target_args += "," + string;
		}
		target_args = target_args.substring(1);
		ret[1] = "+target_args=" + target_args;

		// ret[2] =
		// "+listener=gov.nasa.jpf.listener.PreciseRaceDetector,br.cin.ufpe.Yoshi.YoshiMethodAnalizer";
		ret[2] = "+listener=" + config.getString("listener");
		ret[3] = "+search.class=" + search;
		ret[4] = "+classpath=" + config.getString("classpath");
		ret[5] = "+stop_time=5000";
		return ret;
	}

	static String[] getHeuristicArgs(Config config) {
		String[] ret = new String[5];
		ret[0] = "+target=" + config.getTarget();

		String target_args = "";
		for (String string : config.getTargetArgs()) {
			if (string != null)
				target_args += "," + string;
		}

		target_args = target_args.substring(1);
		ret[1] = "+target_args=" + target_args;

		ret[2] = "+listener=gov.nasa.jpf.listener.PreciseRaceDetector,br.cin.ufpe.Yoshi.YoshiMethodAnalizer";
		ret[3] = "+search.class=br.cin.ufpe.Yoshi.YoshiHeuristicDFS";
		// ret[4] = "+SHOW.STATE.GENERATION=true";
		// ret[4]
		return ret;
	}

	static void dump() {
		// for ( Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo,
		// MethodInfo>> potRaces :
		// YoshiSimplePriorityHeuristic.getInterestings()) {
		// System.out.printf(">\nwrite: %s, %s\nread: %s, %s\n<\n",
		// potRaces.a.a, potRaces.a.b, potRaces.b.a, potRaces.b.b);
		// }
	}

}
